ABS: R-plus(A;B)

STM: R-plus wf

ABS: RplusNoneLeft compseq tag def

ABS: RplusNoneRight compseq tag def

ABS: Rtransform(f;A)

STM: Rtransform wf

ABS: RtransformRplus compseq tag def

ABS: k(v) sends [tg,f(State(ds), v)] on l

STM: Rusends1 wf

ABS: (L)

STM: Rlist wf

ABS: xL.R(x)

STM: Rall wf

STM: Rall-cons

STM: Rall-nil

STM: es realizer-subtype

ABS: pr |= X

STM: sem-sat wf

ABS:  X

STM: sem-satisfiable wf

ABS: K-sem(S;equiv)

STM: K-sem wf

ABS: kpr |= X

STM: K-sem-sat wf

ABS: pr implements kpr

STM: K-implements wf

STM: K-refine

ABS: []!P

STM: box! wf

STM: Rplus-implies

STM: Rnone-implies

ABS: R-size(R)

STM: R-size wf

STM: R-size-implies

STM: R-size-base

STM: R-size-decreases

STM: Rnone?-implies

ABS: R-loc(R)

STM: R-loc wf

ABS: R-has-loc(R;i)

STM: R-has-loc wf

STM: R-has-loc-base

STM: R-has-loc-Rplus

STM: Rlist-has-loc

STM: Rall-has-loc

STM: assert-Rall-has-loc

STM: assert-Rall-has-loc2

ABS: Rds(R)

STM: Rds wf

ABS: R-ds(R;i)

STM: R-ds wf

STM: R-ds-Rds

ABS: Rda(R)

STM: Rda wf

ABS: R-da(R;i)

STM: R-da wf

STM: R-da-Rlist

STM: R-da-Rda

STM: R-da-Rall

ABS: base-domain-type(n)

STM: base-domain-type wf

ABS: p = q

STM: eq bd wf

STM: assert-eq-bd

ABS: R-base-domain(R)

ABS: R-frame-compat(A;B)

STM: R-frame-compat wf

STM: R-frame-compat-self

ABS: Reffect-discrete(A)

STM: Reffect-discrete wf

ABS: Rinit-discrete(A)

STM: Rinit-discrete wf

ABS: R-discrete_compat(A;B)

STM: R-discrete compat wf

STM: R-discrete compat self

STM: R-discrete compat symmetry

STM: R-base-domain wf

ABS: R-interface-compat(A;B)

STM: R-interface-compat wf

ABS: A || B

STM: R-compat wf

ABS: R-icompat(A;B)

STM: R-icompat wf

STM: Rnone-icompat

ABS: R-interface(A;B)

STM: R-interface wf

STM: R-interface-Rplus

STM: R-interface-Rplus2

STM: R-compat-Rplus-sq

STM: R-compat-Rplus2

STM: R-compat-symmetry

STM: R-compat-none

STM: R-compat-Rall

STM: R-compat-Rall2

ABS: R-Feasible(R)

ABS: R-FeasibleWitness

STM: R-FeasibleWitness wf

STM: R-Feasible wf

STM: R-Feasible-Rplus

STM: Rplus-Feasible

STM: R-FeasibleWitness-Rplus

STM: R-FeasibleWitness-compat

STM: R-Feasible-witness

ABS: R-self-interface(R)

STM: R-self-interface wf

STM: R-self-interface-implies

STM: R-Feasible-self-interface

STM: R-interface-compat-self

STM: R-compat-self

STM: Reffect-domain

STM: R-Feasible-effect

ABS: A  B

STM: R-sub wf

ABS: RnoneRsub compseq tag def

STM: R-sub-lemma1

STM: R-sub-self

STM: R-sub-plus-left

STM: R-sub-plus-left2

STM: R-sub-plus-right

STM: R-sub-plus-right2

STM: R-sub-plus-left3

STM: R-sub-plus-right3

STM: R-plus-sub

STM: R-sub transitivity

STM: R-sub-compat

STM: R-compat functionality wrt R-sub

STM: R-compat-sub

STM: R-sub-feasible

STM: R-sub-Rlist

STM: R-sub-Rlist2

STM: R-sub-Rall

STM: R-sub-Rall2

STM: R-feasible-Rlist

STM: R-feasible-Rall

STM: R-compat-Rlist

ABS: pre-init-p(es; i; ds; init; P)

STM: pre-init-p wf

ABS: pre-init-p2(es;i;ds;init;a;p;P)

STM: pre-init-p2 wf

ABS: R-state(R;i)

STM: R-state wf

STM: R-state-plus-cap

STM: R-Feasible-state

STM: Rinit-compat

STM: Rframe-compat

ABS: R-occurs(R;i;z)

STM: R-occurs wf

STM: R-occurs-has-loc

ABS: write-restricted(R;i;k)

STM: write-restricted wf

STM: write-restricted-has-loc

ABS: read-restricted(R; i; y)

STM: read-restricted wf

STM: read-restricted-R-occurs

STM: read-restricted-has-loc

STM: not-R-occurs-frame-compat

STM: not-R-occurs-init-compat

STM: dom-R-ds-occurs

STM: not-R-has-loc-R-ds

STM: not-R-has-loc-R-da

STM: R-compat-disjoint

ABS: R-lnk-tags(ds;da;l;tgs;ks;g)

STM: R-lnk-tags wf

STM: R-lnk-tags-compat2

STM: Rinit-lnk-tags-compat

STM: R-lnk-tags-loc

STM: R-lnk-tags-da

STM: R-compat-ds

STM: R-compat-da

STM: R-compat-da2

STM: R-interface-icompat

STM: R-interface-iff

STM: R-interface-iff2

STM: R-icompat-one-loc

STM: R-icompat-one-loc2

STM: R-icompat-Rplus2

STM: R-icompat symmetry

STM: Rall-icompat

STM: R-icompat-Rall

STM: R-compat-two-loc

STM: R-feasible-Rall-one-loc

ABS: Rinterface(A)

STM: Rinterface wf

STM: Rinterface-Rplus

ABS: interface of plus compseq tag def

STM: Rinterface-icompat

ABS: R-names(A)

STM: R-names wf

ABS: namesRplus compseq tag def

ABS: namesRnone{namesRnone_compseq_tag_def:ObjectId}

STM: Rlist-names

ABS: R-links(A)

STM: R-links wf

ABS: R|names

STM: R-restrict wf

ABS: restrictRplus compseq tag def

STM: trivial-R-restrict

STM: R-restrict-Rnone

STM: R-restrict functionality wrt l contains

STM: R-restrict functionality wrt R-sub

STM: R-restrict functionality

STM: R-base-domain-common-name

STM: Rds-R-names

STM: Rda-R-names

STM: R-frame-compat-disjoint-names

STM: R-discrete-compat-disjoint-names

STM: R-restrict-compat

STM: R-compat-restrict